Nuprl Lemma : merge_wf
11,40
postcript
pdf
T
:Type. subtype_rel(
T
;
)
(
as
,
bs
:(
T
List). merge(
as
;
bs
)
(
T
List))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
,
s-insert(
x
;
l
)
,
reduce(
f
;
k
;
as
)
,
merge(
as
;
bs
)
Lemmas
reduce
wf
,
s-insert
wf
origin
T:Type. subtype_rel(T; 
) 
(as,bs:(T List). merge(as; bs) 
(T List)) T:Type. subtype_rel(T; ) (as,bs:(T List). merge(as; bs) (T List)) Tx:A. B(x) Q